Bell-La Padula model

In computer security, a formal transition model of computer security policy that describes a set of access control rules. In this formal model, the entities in a computer system are divided into abstract sets of subjects and objects. The notion of a secure state is defined, and it is proven that each state transition preserves security by moving from secure state to secure state; thus, inductively proving that the system is secure. A system state is defined to be “secure”, if the only permitted access modes of subjects to objects are in accordance with a specific security policy. In order to determine whether or not a specific access mode is allowed, the clearance of a subject is compared to the classification of the object, and a determination is made as to whether the subject is authorized for the specific access mode. The clearance／classifica- tion scheme is expressed in terms of a lattice.; 計算機安全學中一種計算機安全政策的形式變換模型,描述了一系列存取控制規則。在這 個模型中,一個計算機系統實體被分為主體和客體的抽象集,定義了安全狀態的概念,只在安 全狀態間進行移動,由此證明狀態變遷保證安全性,進而證明系統是安全的。當主體對客體的 容許存取模式與安全性政策一致時,系統狀態定義為“安全”。為確定某個存取模式是否合 法,必須把主體的容許與客體的分類信息進行比較,并決定某種存取模式對主體來說是否合 法。這種容許／分類關系圖是以格子的形式表達的。